Nuprl Lemma : sends-msgs_wf 11,40
A,T:Type, B:(IdType), s:A, v:T, tgf:(tg:Id  (AT(B(tg) List))).
sends-msgs(s; v; tgf)  ((tg:Id  B(tg)) List) 
latex

Definitionst  T, Id, x(s), x:A. B(x), x. t(x), t.2, t.1, map(f; as), sends-msgs(s; v; tg_f)
Lemmasmap wf, pi1 wf, pi2 wf, Id wf

origin